1. Technical Field
The present invention relates to verification of multi-threaded programs and, more particularly, to verification of multi-threaded programs using an asynchronous symbolic approach.
2. Description of the Related Art
Verification of multi-threaded programs is a difficult task due to complex and un-expected interleaving between the threads. In practice, verification efforts often use incomplete methods, or imprecise models, or sometimes both, to address the scalability of the problem. The verification model is typically obtained by composing individual thread models using interleaving semantics. Model checkers are applied to the verification model systematically explore the global state space.
To combat the state explosion problem, most methods employ partial-order reduction techniques to restrict the state-traversal to only a representative subset of all interleavings, thereby avoiding exploring redundant interleaving among independent transitions. Explicit model checkers explore the states and transitions of a concurrent system by explicit enumeration, while symbolic model checkers use symbolic methods. Based on how verifications models are built, symbolic approaches can be broadly classified into: synchronous modeling, which employs a scheduler, and asynchronous modeling, which does not employ a scheduler.
In the synchronous modeling category of symbolic approaches, a synchronous model of concurrent programs is constructed with a scheduler. The scheduler is then constrained by adding guard strengthening to explore only a subset of interleaving. To guarantee correctness and cover all necessary interleavings, the scheduler must permit context-switches between accesses that are conflicting (i.e., dependent). Persistent/ample set computations can be employed to statically determine which pair-wise locations need context switches. Lock-set and/or lock-acquisition history analysis and conditional dependency can also be used to reduce the set of interleavings needed to be explored (i.e., remove redundant interleavings). Even with these state reduction methods, the scalability problem remains. To overcome the problem, researchers have employed sound abstraction with a bounded number of context switches (i.e., under-approximation), while some others have used finite-state model abstractions combined with a proof-guided method to discover the context switches.
In asynchronous category, the symbolic approaches such as Threaded C-Bounded Model Checking (TCBMC) generate verification conditions directly without constructing a synchronous model of concurrent programs, i.e., without using a scheduler. These verification conditions are then solved by satisfiability (SAT) solvers. To knowledge of the inventors, thus far, the state-reduction based on partial-order has hardly been exploited in the asynchronous modeling approaches.